Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> sortSu1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> sortSu1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> sortSu1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
sortSu1(circ2(sortSu1(s), sortSu1(id))) -> sortSu1(s)
sortSu1(circ2(sortSu1(id), sortSu1(s))) -> sortSu1(s)
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
te1(subst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> te1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> sortSu1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> sortSu1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> sortSu1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
sortSu1(circ2(sortSu1(s), sortSu1(id))) -> sortSu1(s)
sortSu1(circ2(sortSu1(id), sortSu1(s))) -> sortSu1(s)
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
te1(subst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> te1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(t), sortSu1(u)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> SORTSU1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> SORTSU1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))

The TRS R consists of the following rules:

sortSu1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> sortSu1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> sortSu1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> sortSu1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
sortSu1(circ2(sortSu1(s), sortSu1(id))) -> sortSu1(s)
sortSu1(circ2(sortSu1(id), sortSu1(s))) -> sortSu1(s)
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
te1(subst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> te1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(t), sortSu1(u)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> SORTSU1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> SORTSU1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))

The TRS R consists of the following rules:

sortSu1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> sortSu1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> sortSu1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> sortSu1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
sortSu1(circ2(sortSu1(s), sortSu1(id))) -> sortSu1(s)
sortSu1(circ2(sortSu1(id), sortSu1(s))) -> sortSu1(s)
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
te1(subst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> te1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 4 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP

Q DP problem:
The TRS P consists of the following rules:

TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> SORTSU1(circ2(sortSu1(t), sortSu1(u)))
TE1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> TE1(msubst2(te1(a), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))
SORTSU1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> SORTSU1(circ2(sortSu1(s), sortSu1(t)))

The TRS R consists of the following rules:

sortSu1(circ2(sortSu1(cons2(te1(a), sortSu1(s))), sortSu1(t))) -> sortSu1(cons2(te1(msubst2(te1(a), sortSu1(t))), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(te1(a), sortSu1(t))))) -> sortSu1(cons2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(cons2(sop1(lift), sortSu1(t))))) -> sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t)))))
sortSu1(circ2(sortSu1(circ2(sortSu1(s), sortSu1(t))), sortSu1(u))) -> sortSu1(circ2(sortSu1(s), sortSu1(circ2(sortSu1(t), sortSu1(u)))))
sortSu1(circ2(sortSu1(s), sortSu1(id))) -> sortSu1(s)
sortSu1(circ2(sortSu1(id), sortSu1(s))) -> sortSu1(s)
sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(s))), sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(t))), sortSu1(u))))) -> sortSu1(circ2(sortSu1(cons2(sop1(lift), sortSu1(circ2(sortSu1(s), sortSu1(t))))), sortSu1(u)))
te1(subst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(a), sortSu1(id))) -> te1(a)
te1(msubst2(te1(msubst2(te1(a), sortSu1(s))), sortSu1(t))) -> te1(msubst2(te1(a), sortSu1(circ2(sortSu1(s), sortSu1(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.